YES(O(1),O(n^5)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^5)). Strict Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) , computeLine(nil(), m, acc) -> acc , computeLine(::(x, xs), nil(), acc) -> nil() , computeLine(::(x, xs), ::(l, ls), acc) -> computeLine(xs, ls, lineMult(x, l, acc)) , matrixMult(nil(), m2) -> nil() , matrixMult(::(l, ls), m2) -> ::(computeLine(l, m2, nil()), matrixMult(ls, m2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^5)) We add following dependency tuples: Strict DPs: { lineMult^#(n, nil(), l2) -> c_1() , lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) , *^#(0(), y) -> c_4() , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) , +^#(0(), y) -> c_6() , +^#(s(x), y) -> c_7(+^#(x, y)) , computeLine^#(nil(), m, acc) -> c_8() , computeLine^#(::(x, xs), nil(), acc) -> c_9() , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_10(computeLine^#(xs, ls, lineMult(x, l, acc)), lineMult^#(x, l, acc)) , matrixMult^#(nil(), m2) -> c_11() , matrixMult^#(::(l, ls), m2) -> c_12(computeLine^#(l, m2, nil()), matrixMult^#(ls, m2)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^5)). Strict DPs: { lineMult^#(n, nil(), l2) -> c_1() , lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) , *^#(0(), y) -> c_4() , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) , +^#(0(), y) -> c_6() , +^#(s(x), y) -> c_7(+^#(x, y)) , computeLine^#(nil(), m, acc) -> c_8() , computeLine^#(::(x, xs), nil(), acc) -> c_9() , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_10(computeLine^#(xs, ls, lineMult(x, l, acc)), lineMult^#(x, l, acc)) , matrixMult^#(nil(), m2) -> c_11() , matrixMult^#(::(l, ls), m2) -> c_12(computeLine^#(l, m2, nil()), matrixMult^#(ls, m2)) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) , computeLine(nil(), m, acc) -> acc , computeLine(::(x, xs), nil(), acc) -> nil() , computeLine(::(x, xs), ::(l, ls), acc) -> computeLine(xs, ls, lineMult(x, l, acc)) , matrixMult(nil(), m2) -> nil() , matrixMult(::(l, ls), m2) -> ::(computeLine(l, m2, nil()), matrixMult(ls, m2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^5)) We estimate the number of application of {1,4,6,8,9,11} by applications of Pre({1,4,6,8,9,11}) = {2,3,5,7,10,12}. Here rules are labeled as follows: DPs: { 1: lineMult^#(n, nil(), l2) -> c_1() , 2: lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , 3: lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) , 4: *^#(0(), y) -> c_4() , 5: *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) , 6: +^#(0(), y) -> c_6() , 7: +^#(s(x), y) -> c_7(+^#(x, y)) , 8: computeLine^#(nil(), m, acc) -> c_8() , 9: computeLine^#(::(x, xs), nil(), acc) -> c_9() , 10: computeLine^#(::(x, xs), ::(l, ls), acc) -> c_10(computeLine^#(xs, ls, lineMult(x, l, acc)), lineMult^#(x, l, acc)) , 11: matrixMult^#(nil(), m2) -> c_11() , 12: matrixMult^#(::(l, ls), m2) -> c_12(computeLine^#(l, m2, nil()), matrixMult^#(ls, m2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^5)). Strict DPs: { lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) , +^#(s(x), y) -> c_7(+^#(x, y)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_10(computeLine^#(xs, ls, lineMult(x, l, acc)), lineMult^#(x, l, acc)) , matrixMult^#(::(l, ls), m2) -> c_12(computeLine^#(l, m2, nil()), matrixMult^#(ls, m2)) } Weak DPs: { lineMult^#(n, nil(), l2) -> c_1() , *^#(0(), y) -> c_4() , +^#(0(), y) -> c_6() , computeLine^#(nil(), m, acc) -> c_8() , computeLine^#(::(x, xs), nil(), acc) -> c_9() , matrixMult^#(nil(), m2) -> c_11() } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) , computeLine(nil(), m, acc) -> acc , computeLine(::(x, xs), nil(), acc) -> nil() , computeLine(::(x, xs), ::(l, ls), acc) -> computeLine(xs, ls, lineMult(x, l, acc)) , matrixMult(nil(), m2) -> nil() , matrixMult(::(l, ls), m2) -> ::(computeLine(l, m2, nil()), matrixMult(ls, m2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^5)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { lineMult^#(n, nil(), l2) -> c_1() , *^#(0(), y) -> c_4() , +^#(0(), y) -> c_6() , computeLine^#(nil(), m, acc) -> c_8() , computeLine^#(::(x, xs), nil(), acc) -> c_9() , matrixMult^#(nil(), m2) -> c_11() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^5)). Strict DPs: { lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) , +^#(s(x), y) -> c_7(+^#(x, y)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_10(computeLine^#(xs, ls, lineMult(x, l, acc)), lineMult^#(x, l, acc)) , matrixMult^#(::(l, ls), m2) -> c_12(computeLine^#(l, m2, nil()), matrixMult^#(ls, m2)) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) , computeLine(nil(), m, acc) -> acc , computeLine(::(x, xs), nil(), acc) -> nil() , computeLine(::(x, xs), ::(l, ls), acc) -> computeLine(xs, ls, lineMult(x, l, acc)) , matrixMult(nil(), m2) -> nil() , matrixMult(::(l, ls), m2) -> ::(computeLine(l, m2, nil()), matrixMult(ls, m2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^5)) We replace rewrite rules by usable rules: Weak Usable Rules: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^5)). Strict DPs: { lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) , +^#(s(x), y) -> c_7(+^#(x, y)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_10(computeLine^#(xs, ls, lineMult(x, l, acc)), lineMult^#(x, l, acc)) , matrixMult^#(::(l, ls), m2) -> c_12(computeLine^#(l, m2, nil()), matrixMult^#(ls, m2)) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^5)) We decompose the input problem according to the dependency graph into the upper component { matrixMult^#(::(l, ls), m2) -> c_12(computeLine^#(l, m2, nil()), matrixMult^#(ls, m2)) } and lower component { lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) , +^#(s(x), y) -> c_7(+^#(x, y)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_10(computeLine^#(xs, ls, lineMult(x, l, acc)), lineMult^#(x, l, acc)) } Further, following extension rules are added to the lower component. { matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) , matrixMult^#(::(l, ls), m2) -> matrixMult^#(ls, m2) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { matrixMult^#(::(l, ls), m2) -> c_12(computeLine^#(l, m2, nil()), matrixMult^#(ls, m2)) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { matrixMult^#(::(l, ls), m2) -> c_12(computeLine^#(l, m2, nil()), matrixMult^#(ls, m2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { matrixMult^#(::(l, ls), m2) -> c_1(matrixMult^#(ls, m2)) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { matrixMult^#(::(l, ls), m2) -> c_1(matrixMult^#(ls, m2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: matrixMult^#(::(l, ls), m2) -> c_1(matrixMult^#(ls, m2)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [nil] = [0] [lineMult](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [1] [*](x1, x2) = [1] x1 + [1] x2 + [0] [+](x1, x2) = [1] x1 + [1] x2 + [0] [0] = [0] [s](x1) = [1] x1 + [0] [computeLine^#](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [matrixMult^#](x1, x2) = [1] x1 + [1] x2 + [0] [c_12](x1, x2) = [1] x1 + [1] x2 + [0] [c] = [0] [c_1](x1) = [1] x1 + [0] This order satisfies following ordering constraints [matrixMult^#(::(l, ls), m2)] = [1] l + [1] ls + [1] m2 + [1] > [1] ls + [1] m2 + [0] = [c_1(matrixMult^#(ls, m2))] The strictly oriented rules are moved into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { matrixMult^#(::(l, ls), m2) -> c_1(matrixMult^#(ls, m2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { matrixMult^#(::(l, ls), m2) -> c_1(matrixMult^#(ls, m2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^4)). Strict DPs: { lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) , +^#(s(x), y) -> c_7(+^#(x, y)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_10(computeLine^#(xs, ls, lineMult(x, l, acc)), lineMult^#(x, l, acc)) } Weak DPs: { matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) , matrixMult^#(::(l, ls), m2) -> matrixMult^#(ls, m2) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^4)) We decompose the input problem according to the dependency graph into the upper component { computeLine^#(::(x, xs), ::(l, ls), acc) -> c_10(computeLine^#(xs, ls, lineMult(x, l, acc)), lineMult^#(x, l, acc)) , matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) , matrixMult^#(::(l, ls), m2) -> matrixMult^#(ls, m2) } and lower component { lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) , +^#(s(x), y) -> c_7(+^#(x, y)) } Further, following extension rules are added to the lower component. { computeLine^#(::(x, xs), ::(l, ls), acc) -> lineMult^#(x, l, acc) , computeLine^#(::(x, xs), ::(l, ls), acc) -> computeLine^#(xs, ls, lineMult(x, l, acc)) , matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) , matrixMult^#(::(l, ls), m2) -> matrixMult^#(ls, m2) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { computeLine^#(::(x, xs), ::(l, ls), acc) -> c_10(computeLine^#(xs, ls, lineMult(x, l, acc)), lineMult^#(x, l, acc)) } Weak DPs: { matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) , matrixMult^#(::(l, ls), m2) -> matrixMult^#(ls, m2) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { computeLine^#(::(x, xs), ::(l, ls), acc) -> c_10(computeLine^#(xs, ls, lineMult(x, l, acc)), lineMult^#(x, l, acc)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { computeLine^#(::(x, xs), ::(l, ls), acc) -> c_1(computeLine^#(xs, ls, lineMult(x, l, acc))) } Weak DPs: { matrixMult^#(::(l, ls), m2) -> c_2(computeLine^#(l, m2, nil())) , matrixMult^#(::(l, ls), m2) -> c_3(matrixMult^#(ls, m2)) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: computeLine^#(::(x, xs), ::(l, ls), acc) -> c_1(computeLine^#(xs, ls, lineMult(x, l, acc))) , 2: matrixMult^#(::(l, ls), m2) -> c_2(computeLine^#(l, m2, nil())) , 3: matrixMult^#(::(l, ls), m2) -> c_3(matrixMult^#(ls, m2)) } Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , +(0(), y) -> y } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [nil] = [0] [lineMult](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] [::](x1, x2) = [1] x1 + [1] x2 + [1] [*](x1, x2) = [1] x1 + [0] [+](x1, x2) = [1] x1 + [1] x2 + [0] [0] = [1] [s](x1) = [1] x1 + [1] [lineMult^#](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [computeLine^#](x1, x2, x3) = [1] x1 + [1] x2 + [0] [c_10](x1, x2) = [1] x1 + [1] x2 + [0] [matrixMult^#](x1, x2) = [1] x1 + [1] x2 + [0] [c] = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] [c_3](x1) = [1] x1 + [0] This order satisfies following ordering constraints [computeLine^#(::(x, xs), ::(l, ls), acc)] = [1] l + [1] ls + [1] x + [1] xs + [2] > [1] ls + [1] xs + [0] = [c_1(computeLine^#(xs, ls, lineMult(x, l, acc)))] [matrixMult^#(::(l, ls), m2)] = [1] l + [1] ls + [1] m2 + [1] > [1] l + [1] m2 + [0] = [c_2(computeLine^#(l, m2, nil()))] [matrixMult^#(::(l, ls), m2)] = [1] l + [1] ls + [1] m2 + [1] > [1] ls + [1] m2 + [0] = [c_3(matrixMult^#(ls, m2))] The strictly oriented rules are moved into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { computeLine^#(::(x, xs), ::(l, ls), acc) -> c_1(computeLine^#(xs, ls, lineMult(x, l, acc))) , matrixMult^#(::(l, ls), m2) -> c_2(computeLine^#(l, m2, nil())) , matrixMult^#(::(l, ls), m2) -> c_3(matrixMult^#(ls, m2)) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { computeLine^#(::(x, xs), ::(l, ls), acc) -> c_1(computeLine^#(xs, ls, lineMult(x, l, acc))) , matrixMult^#(::(l, ls), m2) -> c_2(computeLine^#(l, m2, nil())) , matrixMult^#(::(l, ls), m2) -> c_3(matrixMult^#(ls, m2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^3)). Strict DPs: { lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) , +^#(s(x), y) -> c_7(+^#(x, y)) } Weak DPs: { computeLine^#(::(x, xs), ::(l, ls), acc) -> lineMult^#(x, l, acc) , computeLine^#(::(x, xs), ::(l, ls), acc) -> computeLine^#(xs, ls, lineMult(x, l, acc)) , matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) , matrixMult^#(::(l, ls), m2) -> matrixMult^#(ls, m2) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^3)) We decompose the input problem according to the dependency graph into the upper component { lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> lineMult^#(x, l, acc) , computeLine^#(::(x, xs), ::(l, ls), acc) -> computeLine^#(xs, ls, lineMult(x, l, acc)) , matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) , matrixMult^#(::(l, ls), m2) -> matrixMult^#(ls, m2) } and lower component { lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) , +^#(s(x), y) -> c_7(+^#(x, y)) } Further, following extension rules are added to the lower component. { lineMult^#(n, ::(x, xs), ::(y, ys)) -> lineMult^#(n, xs, ys) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> *^#(x, n) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> +^#(*(x, n), y) , computeLine^#(::(x, xs), ::(l, ls), acc) -> lineMult^#(x, l, acc) , computeLine^#(::(x, xs), ::(l, ls), acc) -> computeLine^#(xs, ls, lineMult(x, l, acc)) , matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) , matrixMult^#(::(l, ls), m2) -> matrixMult^#(ls, m2) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> lineMult^#(x, l, acc) } Weak DPs: { computeLine^#(::(x, xs), ::(l, ls), acc) -> computeLine^#(xs, ls, lineMult(x, l, acc)) , matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) , matrixMult^#(::(l, ls), m2) -> matrixMult^#(ls, m2) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(+^#(*(x, n), y), *^#(x, n), lineMult^#(n, xs, ys)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_1(lineMult^#(n, xs, ys)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_2(lineMult^#(x, l, acc)) } Weak DPs: { computeLine^#(::(x, xs), ::(l, ls), acc) -> c_3(computeLine^#(xs, ls, lineMult(x, l, acc))) , matrixMult^#(::(l, ls), m2) -> c_4(computeLine^#(l, m2, nil())) , matrixMult^#(::(l, ls), m2) -> c_5(matrixMult^#(ls, m2)) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_1(lineMult^#(n, xs, ys)) , 2: computeLine^#(::(x, xs), ::(l, ls), acc) -> c_2(lineMult^#(x, l, acc)) , 3: computeLine^#(::(x, xs), ::(l, ls), acc) -> c_3(computeLine^#(xs, ls, lineMult(x, l, acc))) , 4: matrixMult^#(::(l, ls), m2) -> c_4(computeLine^#(l, m2, nil())) , 5: matrixMult^#(::(l, ls), m2) -> c_5(matrixMult^#(ls, m2)) } Trs: { +(0(), y) -> y } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [nil] = [1] [lineMult](x1, x2, x3) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [1] [*](x1, x2) = [1] x1 + [1] x2 + [0] [+](x1, x2) = [1] x1 + [1] x2 + [0] [0] = [1] [s](x1) = [1] x1 + [1] [lineMult^#](x1, x2, x3) = [1] x2 + [1] [*^#](x1, x2) = [1] x1 + [1] x2 + [0] [c_3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [+^#](x1, x2) = [1] x1 + [1] x2 + [0] [computeLine^#](x1, x2, x3) = [1] x2 + [1] [matrixMult^#](x1, x2) = [1] x1 + [1] x2 + [1] [c] = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] [c_3](x1) = [1] x1 + [0] [c_4](x1) = [1] x1 + [0] [c_5](x1) = [1] x1 + [0] This order satisfies following ordering constraints [lineMult^#(n, ::(x, xs), ::(y, ys))] = [1] x + [1] xs + [2] > [1] xs + [1] = [c_1(lineMult^#(n, xs, ys))] [computeLine^#(::(x, xs), ::(l, ls), acc)] = [1] l + [1] ls + [2] > [1] l + [1] = [c_2(lineMult^#(x, l, acc))] [computeLine^#(::(x, xs), ::(l, ls), acc)] = [1] l + [1] ls + [2] > [1] ls + [1] = [c_3(computeLine^#(xs, ls, lineMult(x, l, acc)))] [matrixMult^#(::(l, ls), m2)] = [1] l + [1] ls + [1] m2 + [2] > [1] m2 + [1] = [c_4(computeLine^#(l, m2, nil()))] [matrixMult^#(::(l, ls), m2)] = [1] l + [1] ls + [1] m2 + [2] > [1] ls + [1] m2 + [1] = [c_5(matrixMult^#(ls, m2))] The strictly oriented rules are moved into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_1(lineMult^#(n, xs, ys)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_2(lineMult^#(x, l, acc)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_3(computeLine^#(xs, ls, lineMult(x, l, acc))) , matrixMult^#(::(l, ls), m2) -> c_4(computeLine^#(l, m2, nil())) , matrixMult^#(::(l, ls), m2) -> c_5(matrixMult^#(ls, m2)) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_1(lineMult^#(n, xs, ys)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_2(lineMult^#(x, l, acc)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_3(computeLine^#(xs, ls, lineMult(x, l, acc))) , matrixMult^#(::(l, ls), m2) -> c_4(computeLine^#(l, m2, nil())) , matrixMult^#(::(l, ls), m2) -> c_5(matrixMult^#(ls, m2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) , +^#(s(x), y) -> c_7(+^#(x, y)) } Weak DPs: { lineMult^#(n, ::(x, xs), ::(y, ys)) -> lineMult^#(n, xs, ys) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> *^#(x, n) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> +^#(*(x, n), y) , computeLine^#(::(x, xs), ::(l, ls), acc) -> lineMult^#(x, l, acc) , computeLine^#(::(x, xs), ::(l, ls), acc) -> computeLine^#(xs, ls, lineMult(x, l, acc)) , matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) , matrixMult^#(::(l, ls), m2) -> matrixMult^#(ls, m2) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'custom shape polynomial interpretation' to orient following rules strictly. DPs: { 3: +^#(s(x), y) -> c_7(+^#(x, y)) , 9: matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_2) = {1, 2}, Uargs(c_5) = {1, 2}, Uargs(c_7) = {1} TcT has computed following constructor-restricted polynomial interpretation. [nil]() = 0 [lineMult](x1, x2, x3) = 0 [::](x1, x2) = x1 + x2 [*](x1, x2) = x1*x2 [+](x1, x2) = x1 + x2 [0]() = 0 [s](x1) = 1 + x1 [lineMult^#](x1, x2, x3) = x1*x2 [c_2](x1, x2) = x1 + x2 [*^#](x1, x2) = x1*x2 [+^#](x1, x2) = x1 [c_5](x1, x2) = x1 + x2 [c_7](x1) = x1 [computeLine^#](x1, x2, x3) = x1*x2 [matrixMult^#](x1, x2) = 1 + x1*x2 + x2 + x2^2 This order satisfies following ordering constraints [*(0(), y)] = >= = [0()] [*(s(x), y)] = y + x*y >= y + x*y = [+(y, *(x, y))] [+(0(), y)] = y >= y = [y] [+(s(x), y)] = 1 + x + y >= 1 + x + y = [s(+(x, y))] [lineMult^#(n, ::(x, xs), nil())] = n*x + n*xs >= x*n + n*xs = [c_2(*^#(x, n), lineMult^#(n, xs, nil()))] [lineMult^#(n, ::(x, xs), ::(y, ys))] = n*x + n*xs >= n*xs = [lineMult^#(n, xs, ys)] [lineMult^#(n, ::(x, xs), ::(y, ys))] = n*x + n*xs >= x*n = [*^#(x, n)] [lineMult^#(n, ::(x, xs), ::(y, ys))] = n*x + n*xs >= x*n = [+^#(*(x, n), y)] [*^#(s(x), y)] = y + x*y >= y + x*y = [c_5(+^#(y, *(x, y)), *^#(x, y))] [+^#(s(x), y)] = 1 + x > x = [c_7(+^#(x, y))] [computeLine^#(::(x, xs), ::(l, ls), acc)] = x*l + x*ls + xs*l + xs*ls >= x*l = [lineMult^#(x, l, acc)] [computeLine^#(::(x, xs), ::(l, ls), acc)] = x*l + x*ls + xs*l + xs*ls >= xs*ls = [computeLine^#(xs, ls, lineMult(x, l, acc))] [matrixMult^#(::(l, ls), m2)] = 1 + l*m2 + ls*m2 + m2 + m2^2 > l*m2 = [computeLine^#(l, m2, nil())] [matrixMult^#(::(l, ls), m2)] = 1 + l*m2 + ls*m2 + m2 + m2^2 >= 1 + ls*m2 + m2 + m2^2 = [matrixMult^#(ls, m2)] The strictly oriented rules are moved into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) } Weak DPs: { lineMult^#(n, ::(x, xs), ::(y, ys)) -> lineMult^#(n, xs, ys) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> *^#(x, n) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> +^#(*(x, n), y) , +^#(s(x), y) -> c_7(+^#(x, y)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> lineMult^#(x, l, acc) , computeLine^#(::(x, xs), ::(l, ls), acc) -> computeLine^#(xs, ls, lineMult(x, l, acc)) , matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) , matrixMult^#(::(l, ls), m2) -> matrixMult^#(ls, m2) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { lineMult^#(n, ::(x, xs), ::(y, ys)) -> +^#(*(x, n), y) , +^#(s(x), y) -> c_7(+^#(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { lineMult^#(n, ::(x, xs), nil()) -> c_2(*^#(x, n), lineMult^#(n, xs, nil())) , *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) } Weak DPs: { lineMult^#(n, ::(x, xs), ::(y, ys)) -> lineMult^#(n, xs, ys) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> *^#(x, n) , computeLine^#(::(x, xs), ::(l, ls), acc) -> lineMult^#(x, l, acc) , computeLine^#(::(x, xs), ::(l, ls), acc) -> computeLine^#(xs, ls, lineMult(x, l, acc)) , matrixMult^#(::(l, ls), m2) -> computeLine^#(l, m2, nil()) , matrixMult^#(::(l, ls), m2) -> matrixMult^#(ls, m2) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { *^#(s(x), y) -> c_5(+^#(y, *(x, y)), *^#(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { lineMult^#(n, ::(x, xs), nil()) -> c_1(*^#(x, n), lineMult^#(n, xs, nil())) , *^#(s(x), y) -> c_2(*^#(x, y)) } Weak DPs: { lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(lineMult^#(n, xs, ys)) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_4(*^#(x, n)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_5(lineMult^#(x, l, acc)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_6(computeLine^#(xs, ls, lineMult(x, l, acc))) , matrixMult^#(::(l, ls), m2) -> c_7(computeLine^#(l, m2, nil())) , matrixMult^#(::(l, ls), m2) -> c_8(matrixMult^#(ls, m2)) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: lineMult^#(n, ::(x, xs), nil()) -> c_1(*^#(x, n), lineMult^#(n, xs, nil())) , 2: *^#(s(x), y) -> c_2(*^#(x, y)) , 3: lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(lineMult^#(n, xs, ys)) , 4: lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_4(*^#(x, n)) , 5: computeLine^#(::(x, xs), ::(l, ls), acc) -> c_5(lineMult^#(x, l, acc)) , 6: computeLine^#(::(x, xs), ::(l, ls), acc) -> c_6(computeLine^#(xs, ls, lineMult(x, l, acc))) , 7: matrixMult^#(::(l, ls), m2) -> c_7(computeLine^#(l, m2, nil())) , 8: matrixMult^#(::(l, ls), m2) -> c_8(matrixMult^#(ls, m2)) } Trs: { lineMult(n, nil(), l2) -> nil() , +(0(), y) -> y } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1, 2}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [nil] = [1] [lineMult](x1, x2, x3) = [1] x1 + [1] x2 + [1] [::](x1, x2) = [1] x1 + [1] x2 + [1] [*](x1, x2) = [1] x1 + [1] x2 + [0] [+](x1, x2) = [1] x1 + [1] x2 + [0] [0] = [1] [s](x1) = [1] x1 + [1] [lineMult^#](x1, x2, x3) = [1] x2 + [1] [c_2](x1, x2) = [1] x1 + [1] x2 + [0] [*^#](x1, x2) = [1] x1 + [0] [+^#](x1, x2) = [1] x1 + [1] x2 + [0] [c_5](x1, x2) = [1] x1 + [1] x2 + [0] [c_7](x1) = [1] x1 + [0] [computeLine^#](x1, x2, x3) = [1] x2 + [1] [matrixMult^#](x1, x2) = [1] x1 + [1] x2 + [1] [c] = [0] [c_1](x1, x2) = [1] x1 + [1] x2 + [0] [c_2](x1) = [1] x1 + [0] [c_3](x1) = [1] x1 + [0] [c_4](x1) = [1] x1 + [0] [c_5](x1) = [1] x1 + [0] [c_6](x1) = [1] x1 + [0] [c_7](x1) = [1] x1 + [0] [c_8](x1) = [1] x1 + [0] This order satisfies following ordering constraints [+(0(), y)] = [1] y + [1] > [1] y + [0] = [y] [+(s(x), y)] = [1] x + [1] y + [1] >= [1] x + [1] y + [1] = [s(+(x, y))] [lineMult^#(n, ::(x, xs), nil())] = [1] x + [1] xs + [2] > [1] x + [1] xs + [1] = [c_1(*^#(x, n), lineMult^#(n, xs, nil()))] [lineMult^#(n, ::(x, xs), ::(y, ys))] = [1] x + [1] xs + [2] > [1] xs + [1] = [c_3(lineMult^#(n, xs, ys))] [lineMult^#(n, ::(x, xs), ::(y, ys))] = [1] x + [1] xs + [2] > [1] x + [0] = [c_4(*^#(x, n))] [*^#(s(x), y)] = [1] x + [1] > [1] x + [0] = [c_2(*^#(x, y))] [computeLine^#(::(x, xs), ::(l, ls), acc)] = [1] l + [1] ls + [2] > [1] l + [1] = [c_5(lineMult^#(x, l, acc))] [computeLine^#(::(x, xs), ::(l, ls), acc)] = [1] l + [1] ls + [2] > [1] ls + [1] = [c_6(computeLine^#(xs, ls, lineMult(x, l, acc)))] [matrixMult^#(::(l, ls), m2)] = [1] l + [1] ls + [1] m2 + [2] > [1] m2 + [1] = [c_7(computeLine^#(l, m2, nil()))] [matrixMult^#(::(l, ls), m2)] = [1] l + [1] ls + [1] m2 + [2] > [1] ls + [1] m2 + [1] = [c_8(matrixMult^#(ls, m2))] The strictly oriented rules are moved into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { lineMult^#(n, ::(x, xs), nil()) -> c_1(*^#(x, n), lineMult^#(n, xs, nil())) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(lineMult^#(n, xs, ys)) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_4(*^#(x, n)) , *^#(s(x), y) -> c_2(*^#(x, y)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_5(lineMult^#(x, l, acc)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_6(computeLine^#(xs, ls, lineMult(x, l, acc))) , matrixMult^#(::(l, ls), m2) -> c_7(computeLine^#(l, m2, nil())) , matrixMult^#(::(l, ls), m2) -> c_8(matrixMult^#(ls, m2)) } Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { lineMult^#(n, ::(x, xs), nil()) -> c_1(*^#(x, n), lineMult^#(n, xs, nil())) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_3(lineMult^#(n, xs, ys)) , lineMult^#(n, ::(x, xs), ::(y, ys)) -> c_4(*^#(x, n)) , *^#(s(x), y) -> c_2(*^#(x, y)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_5(lineMult^#(x, l, acc)) , computeLine^#(::(x, xs), ::(l, ls), acc) -> c_6(computeLine^#(xs, ls, lineMult(x, l, acc))) , matrixMult^#(::(l, ls), m2) -> c_7(computeLine^#(l, m2, nil())) , matrixMult^#(::(l, ls), m2) -> c_8(matrixMult^#(ls, m2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Wall-time: 86.826271s CPU-time: 1059.11599s Hurray, we answered YES(O(1),O(n^5))